T:Type, R:(TT).
WellFnd{i}(T;x,y.R(x,y))
 (x, y:T. Dec(R(x,y)))
 (y:T. L:T List. (x:T. (R(x,y))  (x  L)))
 one-one(T;T;R)
 (y, z:T. (x:T. ((R(x,y))) & ((R(x,z))))  (y = z))
 (a, b:T. ((R^*)(a,b))  ((R^*)(b,a))) 

latex

Definitions	R^*, f(a), left + right, P  Q, x:A. B(x), P & Q, t  T, A, x:AB(x), , x:A  B(x), False, A c B, Type, {T}, WellFnd{i}(A;x,y.R(x;y)), Dec(P), a < b, (x  l), one-one(A;B;R), P  Q, Void, x.A(x), x. t(x), x:A. B(x), x,y. t(x;y), type List, s = t, rel_exp(T;R;n), x f y, {x:A| B(x)} , , #$n, -n, n+m, , n - m, A  B, s ~ t, P  Q, SQType(T)
Lemmas	rel exp-one-one, rel-exp-add-iff, decidable le, nat wf, rel exp wf, le wf, one-one wf, l member wf, decidable wf, wellfounded wf, wellfounded-minimal-field, rel star wf, not wf